package at.fhj.ase;

import java.math.BigDecimal;


public class Article {
	
	private /*@ spec_public @*/ final long artNr;
	private /*@ spec_public @*/ String name;
	private /*@ spec_public @*/ String description;
	private /*@ spec_public @*/ BigDecimal pricePerUnit = new BigDecimal("0");
	private /*@ spec_public @*/ long stock;	
	
	/*@ public normal_behavior
	  @		requires artNr >= 1;
	  @	also requires name != "";
	  @	also requires description != "";
	  @	also requires pricePerUnit != null;
	  @	also requires pricePerUnit.compareTo(new BigDecimal("0")) == 1;	// > 0
	  @*/
	public Article(final long artNr, final String name, final String description, 
			final BigDecimal pricePerUnit) throws IllegalArgumentException {
		if(artNr <= 0 ) {
			throw new IllegalArgumentException("artNr must be >= 1");
		}
		this.artNr = artNr;
		setName(name);
		setDescription(description);
		setPricePerUnit(pricePerUnit);
		
	}
	
	//@ ensures \result ==  artNr;
	protected final long getArtNr() {
		return artNr;
	}
	
	//@ ensures \result == name;
	protected final String getName() {
		return name;
	}

  /* @ protected normal_behavior
	 @		requires name != "";
	 @		requires name.length() >= 5 
	 @	 		&& name.length() <= 25; 
	 @ also protected exceptional_behavior
	 @ also	requires name.length() < 5 || name.length() > 25;
	 @		signals IllegalArgumentException;
	 @ also requires  name == null;
	 @ 		signals NullPointerException;
	 */
	protected final void setName(String name) 
			throws IllegalArgumentException, NullPointerException {
		if(name.length() < 5 || name.length() > 25) {
			throw new IllegalArgumentException("name too short or too long");
		}
				this.name = name;
	}
	
	//@ ensures \result == description;
	public String getDescription() {
		return description;
	}

	/*@ protected normal_behavior 
	  @ 	requires description != null;
	  @	also requires description != "";
	  @*/
	protected void setDescription(String description) 
			throws NullPointerException, IllegalArgumentException {
		if(description == null) {
			throw new NullPointerException("description must not be null");
		}
		if(description == "") {
			throw new IllegalArgumentException("descriptioin must not be empty");
		}
		this.description = description;
	}

	//@ ensures \result == pricePerUnit;
	protected final BigDecimal getPricePerUnit() {
		return pricePerUnit;
	}

	/*@ protected normal_behavior
	  @		requires pricePerUnit != null;
	  @		requires pricePerUnit.compareTo(new BigDecimal("0")) == 1; 
	  @ also protected exceptional_behavior
	  @		requires pricePerUnit == null;
	  @		signals (NullPointerException);
	  @	also requires pricePerUnit.compareTo(new BigDecimal("0")) == -1;
	  @		signals (IllegalArgumentException);
	  @*/
	protected final void setPricePerUnit(BigDecimal pricePerUnit) 
			throws NullPointerException, IllegalArgumentException {
		if(pricePerUnit == null) {
			throw new IllegalArgumentException("pricePerUnit not null");
		}
		if(pricePerUnit.compareTo(new BigDecimal("0")) == -1) {		// < 0
			throw new IllegalArgumentException("pricePerUnit must be >= 0");
		}
		this.pricePerUnit = pricePerUnit;
	}

	//@ ensures \result == stock;
	protected final long getStock() {
		return stock;
	}

	/*@ protected normal_behavior
	  @		requires stock >= 0;
	  @		assignable stock;
	  @	also protected exceptional_behavior
	  @		requires  stock < 0;
	  @		assignable stock;
	  @		signals (IllegalArgumentException);
	 */
	protected final void setStock(long stock) throws IllegalArgumentException {
		if(stock < 0) {
			throw new IllegalArgumentException("stock must not be < 0");
		}
		this.stock = stock;
	}
}
